fetch zf.ax[w78,jmc];
fetch equiv.ax;
fetch equiv.cmd;
exit;show proof;
∀e 2 a;
∃e 3 w;
assume ∀z.(zεw1≡(zεa∧R(x,z)));
assume ∀z.(zεt≡(zεa∧R(x,z)));
∀e EXT w t;
assume zεw;
cancel;
∀e 4 z;
∀e 5 z;
taut zεw≡zεt 7 8;
∀i 9 z;
taut w=t 6 10;
⊃i 5 11;
assume w=t;
tauteq 12:#1 4 13;
show proof 4;
subst 13 4;
subst 13 in 4;
cancel;
substr 13 in 4;
show proof 10:↑;
⊃i 13 14;
 taut 12:#1≡12:#2 12 15;
cancel 14;
subst ↑ in 4;
⊃i 13 14;
taut 12:#1≡12:#2 12 15;
show prf;
∃i 16 t→z;
∃i 16 t←z;
cancel;
show prf;
∀i ↑ t;
∃i 17 t→y;
∃i 17 t←y;
show prf;
cancel;
∃i 17 w←y;
show prf;
∀i 18 x;
show prf;
taut 1:#2 1 19;
show proof→equiv.prf;
∀e 20 a;
show proof 2;
show proof 1
;
exit;fetch equiv.cmd;fetch z2.ax[w78,jmc];
fetch zf.ax[w78,jmc];
fetch equiv.ax;
fetch equiv1.cmd;
fetch equiv2.cmd;
∀e 20 a;
show proof→equiv.fetch zf.ax[w78,jmc];fetch zf.ax[w78,jmc];
fetch equiv.ax;
fetch equiv2.cmd;
∃e 21 v;
∀e UNION v;
cancel;FETCH ZF.AX[W78,JMC];
FETCH EQUIV.AX;
FETCH EQUIV2.CMD;
∃e 21 v;
∀e UNION v;
∀e 23 z;
assume zε union v;
taut 24:#2 24 25;
∃e 26 t;
∀e 22 t;
taut 28:#2 27 28;
∃e 29 s;
∧e 30 2
;
∀e 31 z;
taut zεa 27 32;
show proof 22:25;
⊃i 25 33;
show proof→equiv.prf;
assume zεa;
∧i SEP[λy.(yεa∧R(z,y))];
∧i SEP[B←λy.(yεa∧R(z,y))];
cancel;
∧i SEP[B←λy.R(z,y)];
∀e 36 a;
∃e 37 y;
show proof 22;
∧i 35 38;
∃i 39[s←z];
∃i 39[z←s];
∃i 39,z←s;
∀e 22 y;
taut yεv 40 41;
show prf;
∀e 38 z;
∀e reflex z;
∀e REFLEX z;
show axioms;
show prf;
∀e EQUIV1 z;
taut zεy 33 43 44;
∧i 42 45;
∃i 46 y←t;
show prf;
show prf 23:24;
taut zε union v 24 47;
⊃i 35 48;
show proof 25;
show proof 33;
cancel;
cancel;
show prf;
cancel 45;
taut zεy 35 43 44;
∧i 42 45;
∃i 46 y←t;
show prf 23:25;
taut zεunion v 47 24;
⊃i 35 48;
show prf 22:↑;
taut zεa≡zεunion v 34 49;
∀i 50 z;
cancel 50;
taut zεunion v≡zεa 34 49;
∀i 50 z;
∀e EXT union v a;
taut union v = a 51 52;
show proof→equiv.prf;
declare INDVAR r1 r2;
assume r1εv;
assume r2εv;
cancel 54;
assume r1εv∧r2εv;
assume xεr1∩r2;
cancel;
assume ∃x.(xεr1 ∧ xεr2);
∃e 55 x;
assume yεr1;
show prf 22;
show prf 22,54:↑;
∀e 22 r1;
taut 58:#2 54 58;
∃e 59 s;
∧e 60 2;
exit;show prf 54:↑;
∀e 61 y;
∀e 61 x;
∀e EQUIV2 x s;
cancel;
∀e EQUIV2 s x;
∀e EQUIV3 x s y;
taut R(x,y)  65 64 63 62 55 56;
show prf 54:↑;
taut R(x,y) 62:65 56 57;
⊃i 57 66;
cancel 54;
assume rεv;
show prf 22;
∀e 22 r;
taut 55:#2 54 55;
assume xεr∧yεr;
∃e 56 s;
∧e 58 2;
∀e 59 x;
∀e 59 y;
∀e EQUIV2 s x;
∀e EQUIV3 x s y;
show prf 54:↑;
taut R(x,y) 60:63 57;
⊃i 57 64;
∀i 65 x y;
⊃i 54 66;
∀i 67  r;
show proof→equiv.prf;
exit;fetch zf.ax[w79,jmc];
fetch zf.ax[w78,jmc];
fetch equiv.ax;
fetch equiv.cmd;
cancel 1;
fetch equiv1.cmd;
fetch equiv2.cmd;fetch zf.ax[w78,jmc];
fetch equiv.ax;
fetch equiv2.cmd;
∧i SEP[B←λy.R(s,y)];
cancel 1;
fetch equiv2.ax;
fetch equiv2.cmd;
show proof 35:↑;
cancel 1;
fetch equiv2.cmd;
show proof 42:↑;
show proof 35;
cancel 1;
fetch equiv2.cmd;
fetch equiv2.cmd;
exit;show proof→equiv.prf;
show proof 22;
assume r1εv;
assume r2εv;
assume xεr1∧xεr2;
assume wεr1;
∀e 22 r1;
∀e 22 r2;
taut 73:#2 69 73;
taut 74:#2 70 74;
∃e 75 s;
∃e 76 t;
∧e 77 2;
∧e 78 2;
∀e 79 x;
∀e 80 x;
show prf 69:↑;
taut R(s,x) 71 81;
taut R(t,x) 71 82;
∀e 79 w;
∀e 80 w;
show prf 69:↑;
∀e EQUIV2 s x;
∀e EQUIV3 t x s;
∀e EQUIV3 t s w;
show prf 69:↑;
taut wεr2 71 72 81:↑;
cancel;
∀e EQUIV3 s x t;
∀e EQUIV3 s t w;
taut wεr1≡wεr2 71 81:↑;
cancel 90;
taut wεr2 71 72 81:↑;
⊃i 72 90;
∀i 91 w;
⊃i 70 92;
show prf 69:71;
⊃i 69 93;
⊃i 71 94;
∀i 95 x;
∀i 96 r1 r2;
cancel 96;
∀i 95 r1 r2 x;
∀e 96 r2 r1 x;
show prf 85:↑;
assume r1εv ∧ r2εv ∧xεr1 ∧ xεr2;
taut ∀w.(wεr1 ⊃ wεr2) 98 95;
∀e 99 w;
taut ∀w.(wεr2 ⊃ wεr1) 97 98;
∀e 101 w
;
taut wεr1≡wεr2 100 102;
∀i 103 w;
∀e EXT r1 r2;
taut r1=r2 104 105;
⊃i 98 106;
Assume ∃x.B(x)⊃A(a,a);
ASSUME ∀x.(B(x)⊃A(a,a));
ASSUME ∃x.(B(x));
∃e ↑ x;
∀e ↑↑↑ x;
⊃e 110,111;
⊃i 109⊃↑;
show prf 108:↑;
show prf 104:↑;
cancel 108;
assume r1εv∧r2εv;
taut xεr1∧xεr2 ⊃r1=r2 108 107;
∀i 109 x;
assume ∃x.(xεr1∧xεr2);
∃e 111 x;
∀e 110 x;
⊃e 112 113;
⊃i 111 114;
⊃i 108 115;
taut 116:#1∧116:#2#1⊃116:#2#2 116;
∀i 117 r1 r2;
show prf 22;
taut 53:∧68:∧118: 53 68 118;
show prf 21;
∀i 119 v;
⊃i 22 119;
∀i v 120;
∀i 120 v;
cancel;
cancel 120;
show prf 21 22 119;
∃i 119 v;
show proof→equiv.prf;
exit;fetch zf.ax[w78,jmc];
fetch equiv.ax;
fetch equiv.cmd;
show proof→equiv.prf;
exit;cancel 69;
fetch equiv2.cmd from 0 to 1;
fetch equiv1.cmd from 0 to 1;
fetch equiv2.cmd from 0 to 1;
cancel 69;
fetch equiv2.cmd from 0 to 1;
fetch equiv2.cmd from 0 to 1;
cancel 74;
fetch equiv2.ax from 0 to 1;
fetch equiv2.cmd from 0 to 1;
fetch equiv2.cmd from 0 to 1;
fetch equiv2.cmd from 0 to 1;
show prf 69:↑;
show prf 69 70 79 80→foo;
fetch equiv2.cmd from 0 to 1;
show prf 80 81→foo.1;
show prf 82→foo.1;
fetch equiv.ax;
show prf 69:↑;
fetch equiv2.cmd from 0 to 1;
fetch equiv2.cmd from 0 to 1;
show prf 80:↑;
cancel 84;
cancel;
show prf 79:↑;
fetch equiv2.cmd from 0 to 1;
cancel 83;
fetch equiv2.cmd from 0 to 1;
cancel 83;
show prf 79:↑;
fetch equiv2.cmd from 0 to 1;
cancel 83;
fetch equiv2.cmd from 0 to 1;
cancel 83;
fetch equiv2.cmd from 0 to 1;
cancel 83;
show prf 79:82;
h;
fetch equiv2.cmd from 0 to 1;
fetch equiv2.cmd from 0 to 1;
show prf 69 70;
cancel;
fetch equiv2.cmd from 0 to 1;
cancel 94;
show prf 90:↑;
fetch equiv2.cmd from 0 to 1;
taut r1=r2 93 94;
cancel;
h;
fetch equiv2.cmd from 0 to 1;
cancel;
fetch equiv2.cmd from 0 to 1;
show prf 69;
fetch equiv2.cmd from 0 to 1;
fetch equiv2.cmd from 0 to 1;
fetch equiv2.cmd from 0 to 1;
∀i ↑ a;
exit;fetch zf.ax[w78,jmc];fetch zf.ax[w78,jmc];
fetch equiv.ax;
fetch equiv2.cmd;
show proof→equiv.fetch zf.ax[w78,jmc]
;
fetch equiv.ax;
fetch lose.cmd;
fetch equiv.cmd;∧i REPL[A←λx t.(∀y.(yεt ≡ yεa ∧ R(x,y)))];
∧i SEP[B←λy.R(x,y)];
∀E ↑ a;
∃E ↑ w;show prf 1:2→lose.fetch lose.prf;fetch lose.prf;fetch lose.prf;
⊃e ↑ ↑↑;
⊃e 3 2;
∃e 4 x;
tauteq false 5;
tauteq FALSE 5;
show proof;
show proof→false.FETCH LOSE.PRF;
SHOW PRF→FALSE.fetch lose.prf;fetch test.ax;fetch test.ax;
axiom foo1: ∃x.B(x);;
∧i foo[B←λx y.(f(x,y) = f(y,x))];
∧i foo[B←λx.λy.(f(x,y) = f(y,x))];
∧i foo[B←λx r.(f(x,y) = f(y,x))];
∧i foo[B←λx r.(f(x,r) = f(r,x))];fetch test.ax;
∧i foo2[B←λs t.¬(s=t)];